Problem:
 i(0(x1)) -> p(s(p(s(0(p(s(p(s(x1)))))))))
 i(s(x1)) -> p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x1))))))))))))))))))
 j(0(x1)) -> p(s(p(p(s(s(0(p(s(p(s(x1)))))))))))
 j(s(x1)) -> s(s(s(s(p(p(s(s(i(p(s(p(s(x1)))))))))))))
 p(p(s(x1))) -> p(x1)
 p(s(x1)) -> x1
 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1)))))))))

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {5,4,3}
   transitions:
    01(20) -> 21*
    01(94) -> 95*
    s1(45) -> 46*
    s1(92) -> 93*
    s1(87) -> 88*
    s1(82) -> 83*
    s1(44) -> 45*
    s1(91) -> 92*
    s1(86) -> 87*
    s1(81) -> 82*
    s1(61) -> 62*
    s1(56) -> 57*
    s1(51) -> 52*
    s1(46) -> 47*
    s1(26) -> 27*
    s1(21) -> 22*
    s1(16) -> 17*
    s1(93) -> 94*
    s1(88) -> 89*
    s1(58) -> 59*
    s1(53) -> 54*
    s1(23) -> 24*
    s1(18) -> 19*
    s1(90) -> 91*
    s1(85) -> 86*
    p1(60) -> 61*
    p1(50) -> 51*
    p1(62) -> 63*
    p1(52) -> 53*
    p1(47) -> 48*
    p1(22) -> 23*
    p1(17) -> 18*
    p1(84) -> 85*
    p1(59) -> 60*
    p1(54) -> 55*
    p1(49) -> 50*
    p1(24) -> 25*
    p1(19) -> 20*
    p1(83) -> 84*
    p1(48) -> 49*
    i1(80) -> 81*
    j1(55) -> 56*
    p2(112) -> 113*
    p2(104) -> 105*
    p2(116) -> 117*
    p2(106) -> 107*
    p2(120) -> 121*
    i0(2) -> 3*
    i0(1) -> 3*
    00(2) -> 1*
    00(1) -> 1*
    p0(2) -> 5*
    p0(1) -> 5*
    s0(2) -> 2*
    s0(1) -> 2*
    j0(2) -> 4*
    j0(1) -> 4*
    1 -> 5,26
    2 -> 5,16
    16 -> 121,18
    17 -> 44*
    18 -> 20,80
    20 -> 80*
    21 -> 113,61,23
    22 -> 58*
    23 -> 25,3
    25 -> 81,3
    26 -> 121,18
    27 -> 17*
    44 -> 117,120
    45 -> 107,49,116
    46 -> 48,106
    47 -> 90*
    51 -> 53*
    53 -> 55*
    57 -> 21*
    58 -> 60,112
    61 -> 63,4
    63 -> 56,4
    81 -> 105*
    82 -> 84,104
    89 -> 56,4
    95 -> 5*
    105 -> 85*
    107 -> 49*
    113 -> 61*
    117 -> 50*
    121 -> 51,53,55
  problem:
   
  Qed